(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun g () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun h () String)
(assert (= "escapex3e" c))
(assert (= "escapex3cescapex2fescapex74escapex65escapex78escapex74escapex61escapex72escapex65escapex3eescapex0descapex0a" d))
(assert (= (str.++ c a d) g))
(assert (= e "escapex3cescapex73escapex65escapex6cescapex65escapex63escapex74escapex20escapex6eescapex61escapex6descapex65escapex3descapex27escapex62escapex62escapex63escapex6fescapex6cescapex6fescapex6cescapex65escapex3descapex27escapex77escapex69escapex64escapex74escapex68escapex3aescapex39escapex30escapex70escapex78escapex3bescapex27escapex20escapex6fescapex6eescapex43escapex68escapex61escapex74escapex28escapex27escapex6descapex65escapex73escapex73escapex61escapex67escapex65escapex27escapex2cescapex20escapex27escapex5bescapex63escapex6fescapex6cescapex6fescapex72escapex3descapex27escapex20escapex2bescapex20escapex74escapex68escapex69escapex73escapex2eescapex6fescapex70escapex74escapex75escapex65escapex3descapex27escapex6descapex61escapex72escapex6fescapex6fescapex6eescapex27escapex20escapex73escapex74escapex79escapex6cescapex65escapex3descapex27escapex63escapex6fescapex6cescapex6fescapex72escapex3aescapex6descapex61escapex72escapex6fescapex6fescapex6eescapex3bescapex27escapex3eescapex4descapex61escapex72escapex6fescapex6fescapex6eescapex3cescapex2fescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex3eescapex0descapex0aescapex3cescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex20escapex76escapex61escapex6cescapex75escapex65escapex3descapex27escapex72escapex65escapex64escapex27escapex20escapex73escapex74escapex79escapex6cescapex65escapex3descapex27escapex63escapex6fescapex6cescapex6fescapex72escapex3aescapex72escapex65escapex64escapex3bescapex27escapex3eescapex52escapex65escapex64escapex3cescapex2fescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex3eescapex0descapex0aescapex3cescapex6fescapex70escapex74escapex69escapex6fescapex6eescapex20escapex76escapex61escapex6cescapex75escapex65escapex3descapex27escapex6fescapex72escapex61escapex6eescapex67escapex65escapex27escapex20escapex73escapex74escapex79escapex6cescapex65escaescapex62escapex6cescapex32escapex27escapex3eescapex0descapex0a"))
(assert (= (str.++ g e) f))
(assert (= h (str.++ f b)))
(assert (str.in_re h (re.++ (re.* re.allchar) (str.to_re "escapex5c") (re.* re.allchar))))
(check-sat)
